Programación Avanzada

1 Contenido de la clase

Regla de inferencia del if con else Pág. 101-107

Para demostrar la corrección de if B then C1 else C2 con precondición {P} y poscondición {Q} hay que demostrar dos cosas:

• { P ∧ B } C1 { Q } (cuando la condición es verdadera se ejecuta C1).
• { P ∧ ¬B } C2 { Q } (cuando es falsa se ejecuta C2).

{P ∧ B} C1 {Q} ; {P ∧ ¬B} C2 {Q} ⇒ {P} if B then C1 else C2 {Q}

Ejemplo: máximo de dos números. Demostrar que es correcta la terna

{ } if a > b then m := a else m := b { (m ≥ a) ∧ (m ≥ b) }

Intuitivamente: si a > b → m := a > b → { m = a ∧ m > b }; si ¬(a > b) (es decir b ≥ a) → m := b ≥ a → { m = b ∧ m ≥ a }. En ambos casos m obtiene el mayor de a y b.

• Caso verdadero: se demuestra { a > b } m := a { (m ≥ a) ∧ (m ≥ b) }. Por la regla de la asignación, la precondición es { (a ≥ a) ∧ (a ≥ b) }; como { a > b } ⇒ { a ≥ a ∧ a ≥ b }, se concluye (q.l.q.d.).
• Caso falso: se demuestra { ¬(a > b) } m := b { (m ≥ a) ∧ (m ≥ b) }. La precondición por asignación es { (b ≥ a) ∧ (b ≥ b) }, y como { ¬(a > b) } = { b ≥ a }, se concluye (q.l.q.d.).
• Finalmente, aplicando la regla del if con else a ambos casos, la terna es correcta (q.l.q.d.).

Segundo ejemplo: demostrar { a > b } if a > b then m := a else m := b { m = a }.

• Intuitivamente, como a > b, se ejecuta m := a, por lo que m = a.
• Caso verdadero: se demuestra { a > b } m := a { m = a } (la precondición por asignación es { a = a } = { }).
• Caso falso: se demuestra { ¬(a > b) } m := b { m = a }. La precondición por asignación es { b = a }, y como { ¬(a > b) } (junto a ¬(b > a)) implica { b = a }, se concluye.
• Aplicando la regla del if con else, la terna es correcta.

Verificación de ciclos. Inducción matemática Pág. 108

Para demostrar la corrección de un ciclo se usa la inducción matemática:

• Sea k un entero fijo (positivo, negativo o cero). Para cada entero n ≥ k hay una proposición P(n) y se desea demostrar que es verdadera para todo n ≥ k.
• Paso básico o paso base: P(k) es verdadera.
• Paso inductivo: para n ≥ k, siempre que P(n) sea verdadera (hipótesis de inducción), se sigue que P(n + 1) es verdadera.
• Entonces el principio de inducción matemática establece que P(n) es verdadera para todo n ≥ k.

Ejemplo: la función Cuadrado(A) Pág. 109-112

Seudocódigo:

Function Cuadrado(A) ; C ← 0 ; D ← 0 ; While (D ≠ A) ; C ← C + A ; D ← D + 1 ; Return C

Se demuestra que esta función calcula el cuadrado de un entero positivo A. Sean C_n y D_n los valores de C y D tras pasar n veces por el ciclo:

• C_0 = 0, C_1 = A, C_2 = 2A, C_3 = 3A, … → se conjetura que C_n = n·A.
• D_0 = 0, D_1 = 1, D_2 = 2, … → D_n = n.
• Sea P(n) el enunciado C_n = n·A; se prueba por inducción con k = 0.

• Paso base (n = 0): C_0 = 0·A = 0, que es cierto porque C_0 = 0.
• Hipótesis de inducción: supongamos C_n = n·A.
• Paso inductivo (n + 1): tras pasar una vez más por el ciclo, a C se le suma A y a D se le suma 1: C_{n+1} = C_n + A = n·A + A = A(n + 1). Así P(n + 1) es verdadera.

Por el principio de inducción, siempre que el ciclo ocurre se cumple C_n = n·A. Cuando el ciclo termina, D_n = A, y como D_n = n, entonces n = A y C = A·A = A². Por lo tanto la función regresa el cuadrado de A.

Invariante de un ciclo Pág. 113

Un invariante de un ciclo es una relación entre variables que persiste a través de todas las iteraciones del ciclo, antes y después de ejecutarlo. En el ejemplo anterior, el invariante del ciclo es C_n = n·A (o equivalentemente C = D·A).

Ejemplo: subrutina que calcula N^M Pág. 113-117

Seudocódigo:

Subroutine (N, M; R) ; R ← 1 ; While (M > 0) ; R ← R × N ; M ← M – 1 ; Return

N y M son enteros no negativos y la rutina regresa el valor de R. Sean R_n y M_n los valores de R y M tras pasar n veces por el ciclo:

• R_0 = 1, R_1 = N, R_2 = N², … → R_n = N^n.
• M_0 = M, M_1 = M − 1, M_2 = M − 2, … → M_n = M − n.
• De M_n = M − n se tiene n = M − M_n, y sustituyendo: R_n = N^{M − M_n}, es decir R_n · N^{M_n} = N^M. Este es el invariante del ciclo.
• Sea P(n) el enunciado R_n = N^{M − M_n}; se prueba por inducción con k = 0.

• Paso base (n = 0): R_0 = 1 y N^{M − M_0} = N^{M − M} = N^0 = 1. Cierto.
• Hipótesis de inducción: R_n = N^{M − M_n}.
• Paso inductivo (n + 1): tras una iteración más, a R se le multiplica por N y a M se le resta 1: R_{n+1} = R_n × N = N^{M − M_n} × N …; como M_{n+1} = M_n − 1, se obtiene R_{n+1} = N^{M − M_{n+1}}. Así P(n + 1) es verdadera.

Cuando el ciclo termina, M_n = 0, y entonces R = N^{M − 0} = N^M. Por lo tanto la subrutina calcula N a la M (potencia N^M).

2 Puntos destacados / Lo que hay que saber

3 Actividades y tareas pendientes

En esta clase (Nota 6) no se dejó una tarea nueva: la conferencia desarrolla la regla del if con else y la verificación de ciclos con inducción.

Queda pendiente de entregar la tarea de la Nota 4:

4 Dudas que podrían examinar

5 Sitios o recursos para visitar

En esta clase no se mencionaron sitios ni recursos específicos.

6 Glosario de términos

• Regla del if con else: si {P ∧ B} C1 {Q} y {P ∧ ¬B} C2 {Q} son correctas, entonces {P} if B then C1 else C2 {Q} es correcto.
• Regla de la asignación: al calcular precondiciones se sustituye en la poscondición el valor que toma la variable tras la asignación.
• Inducción matemática: paso base P(k) + paso inductivo P(n) ⇒ P(n + 1) ⇒ P(n) para todo n ≥ k.
• Paso base (de la inducción): demostrar que P(k) es verdadera para el valor inicial k.
• Paso inductivo: demostrar que, si P(n) es verdadera (hipótesis de inducción), entonces P(n + 1) lo es.
• Hipótesis de inducción: suponer que P(n) es verdadera para una n dada, para probar el paso inductivo.
• Invariante de un ciclo: relación entre variables que persiste a través de todas las iteraciones, antes y después del ciclo.
• Verificación de ciclos: demostración (por inducción) de que un ciclo cumple su invariante y produce el resultado esperado al terminar.
• Traza del ciclo: valores que toman las variables en cada iteración (C₀, C₁, …, R₀, R₁, …, M₀, M₁, …).

7 Mapa mental textual

• Programación Avanzada · Clase 6 · Verificación de programas (Nota 6)
  • Regla del if con else
    • {P ∧ B} C1 {Q} y {P ∧ ¬B} C2 {Q} ⇒ {P} if B then C1 else C2 {Q}
    • Ej.: máximo de dos números (m obtiene el mayor de a y b)
    • Ej.: {a>b} if a>b then m:=a else m:=b {m=a}
  • Verificación de ciclos · Inducción matemática
    • Paso base P(k) + paso inductivo P(n) ⇒ P(n+1) ⇒ P(n) ∀ n ≥ k
    • Función Cuadrado(A) (cuadrado de A)
    • Traza: C₀=0, C₁=A, C₂=2A, …; D₀=0, D₁=1, …
    • Conjetura: C_n = n·A
    • Invariante del ciclo: C = D·A
    • Al terminar (D=A): C = A²
  • Invariante de un ciclo
    • Relación que persiste en todas las iteraciones
  • Subrutina de potencia (N^M)
    • Ciclo: R ← R×N; M ← M−1
    • Traza: R₀=1, R₁=N, R₂=N², …; M₀=M, M₁=M−1, …
    • Invariante: R_n · N^{M_n} = N^M (equiv. R_n = N^{M − M_n})
    • Al terminar (M=0): R = N^M